Beta reduction（β-归约）是λ演算（lambda calculus）中的核心化简规则：把函数应用“展开”成把实参代入函数体的过程。形式上常写作：
[
(\lambda x., M), N ;\to; M[x := N]
]
即“把 (N) 替换到 (M) 中所有自由出现的 (x)”。（在编程语言中，这常对应于函数调用/求值的一步。）
/ˈbeɪtə rɪˈdʌkʃən/
In lambda calculus, beta reduction replaces a function parameter with an argument.
在λ演算中，β-归约会用实参替换函数形参。
After several steps of beta reduction, the expression reaches normal form without any reducible parts.
经过若干步β-归约后，这个表达式到达正规形（normal form），不再包含可继续化简的部分。
“Beta”来自希腊字母 β，用于在形式系统中给不同规则/变换做标记；“reduction”源自拉丁语 reducere（“带回、还原”），在数学与逻辑中常指把表达式化简到更基本的形式。β-归约这一命名传统与λ演算早期文献的符号体系有关。
Select Language